﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Automata\MM\MealyMachine.cs
 * Description  :     Implementation of Mealy machine sructure 
 * Change log   :     -Dec 2012:  First version
 * To Do        :    
 ************************************************************************/
using System;
using System.Collections.Generic;

using SMLib.Automata.Base;
using SMLib.Utils;
using SMLib.Base;
using SMLib.Interoperability.DOT;

namespace SMLib.Automata.MM
{
    /// <summary>
    /// Defenition of a Mealy Machine.
    /// Essentially, a mealy machine is a set of mealy nodes plus the input/output alphabet
    /// (it can be deterministic OR non-deterministic)
    /// </summary>
    public class MealyMachine : DiGraph<MealyMachine.Mealy_State, MealyMachine.Mealy_Transition>
    {
        #region Mealy Node
        /// <summary>
        /// Defenition of Mealy Node
        /// </summary>
        public class Mealy_State : IState<Mealy_Transition>
        {
            /// <summary>
            /// Use refrence for equality check. If it is true, the "Equals" method 
            /// works based on equality of references (instead of equality of content of objects)
            /// </summary>
            public static bool UseRefForEquality = true;

            /// Identifiers of nodes are "string"
            string id = "";
            List<Mealy_Transition> tr;

            public Mealy_State(string ID)
            {
                id = ID;
                tr = new List<Mealy_Transition>();
            }

			public void ChangeID(string id)
			{
				this.id = id;
			}

            /// <summary>
            /// We consider two states equal iff they have same ID
            /// <seealso cref="UseRefForEquality"/>
            /// </summary>
            /// <param name="obj">the other object to be compared with</param>
            /// <returns>true if they are equal, false in other case</returns>
            public override bool Equals(object obj)
            {
                if (UseRefForEquality)
                {
                    return object.ReferenceEquals(this, obj);
                }
                if (obj is Mealy_State)
                {
                    return (((Mealy_State)obj).id == id);
                }
                return false;
            }

            /// <summary>
            /// Return list of all outputs for a specific input (in nondeterministic mealy machines)
            /// </summary>
            /// <param name="input"></param>
            /// <returns></returns>
            public List<ISymbol> ListOfAllOutputs(ISymbol input)
            {
                List<ISymbol> outputs = new List<ISymbol>();

                foreach (Mealy_Transition t in Transitions)
                {
                    if (t.inLabel.Equals(input))
                        outputs.Add(t.outLabel);
                }
                return outputs;
            }

            public bool HasTransitionTo(Mealy_State n)
            {
                foreach (Mealy_Transition t in Transitions)
                    if (t.Destination == n)
                        return true;
                return false;
            }
            /// <summary>
            /// Return list of all input/outputs
            /// </summary>
            /// <returns></returns>
            public List<PairOfSymbols> ListOfAllInputOutputs()
            {
                List<PairOfSymbols> ios = new List<PairOfSymbols>();
                foreach (Mealy_Transition t in Transitions)
                {
                    PairOfSymbols ps = t.Label;// new PairOfStringSymbols(t.inLabel, t.outLabel);
                    bool existInList = false;
                    foreach (PairOfSymbols ps2 in ios)
                        if (
                            /*((KeyValuePair<string, string>)ps2.userObject).Key*/ //ps2.Key == t.inLabel 
                            ps2.Input.Equals(t.inLabel)
                            &&
                            /*((KeyValuePair<string, string>)ps2.userObject).Value*/ //ps2.Val == t.outLabel
                            ps2.Output.Equals(t.outLabel)
                            )
                        {
                            existInList = true;
                            break;
                        }

                    if (!existInList)
                        ios.Add(ps);
                }
                return ios;
            }

            /// <summary>
            /// Return list of all next nodes for an input (AND optionaly, for a specific output)
            /// For deterministic Mealy machine, use "NextNode" instead.
            /// </summary>
            /// <param name="input"></param>
            /// <param name="output"></param>
            /// <returns></returns>
            public List<Mealy_State> ListOfAllNextNodes(ISymbol input, ISymbol output = null)
            {
                List<Mealy_State> nodes = new List<Mealy_State>();
                foreach (Mealy_Transition t in Transitions)
                {
                    if (output == null)
                    {
                        if (t.inLabel.Equals(input))
                            nodes.Add((Mealy_State)t.Destination);
                    }
                    else
                        if (t.inLabel.Equals(input) && t.outLabel.Equals(output))
                        {
                            nodes.Add((Mealy_State)t.Destination);
                        }
                }
                return nodes;
            }

            /// <summary>
            /// It should be deterministic!
            /// For nondeterministic Mealy machine, use "ListOfAllNextNodes" instead.
            /// </summary>
            /// <returns></returns>
            public Mealy_State NextNode(ISymbol input, ISymbol output = null)
            {
                foreach (Mealy_Transition t in Transitions)
                {
                    if (output == null)
                    {
                        if (t.inLabel.Equals(input))
                            return (Mealy_State)t.Destination;
                    }
                    else
                        if (t.inLabel.Equals(input) && t.outLabel.Equals(output))
                        {
                            return (Mealy_State)t.Destination;
                        }
                }
                return null;
            }

            public Mealy_State NextNode(ISymbol input, out ISymbol output)
            {
                foreach (Mealy_Transition t in Transitions)
                {
                    if (t.inLabel.Equals(input))
                    {
                        output = t.outLabel;
                        return (Mealy_State)t.Destination;
                    }
                }
                output = null;
                return null;
            }


            /// <summary>
            /// Add a transition to the state (it will always add the transition and doesn't care about determinisim)
            /// </summary>
            /// <param name="dest">destination of transition</param>
            /// <param name="symb">symbol on the transition</param>
            /// <returns>the added transition</returns>
            public Mealy_Transition AddTransition(Mealy_State dest, PairOfSymbols symb)
            {
                Mealy_Transition t = new Mealy_Transition(symb.Input, symb.Output);
                t.SetDestination(dest);
                tr.Add(t);
                return t;
            }


            public Mealy_Transition AddTransition(Mealy_State dest, ISymbol input, ISymbol output)
            {
                Mealy_Transition t = new Mealy_Transition(input, output);
                t.SetDestination(dest);
                tr.Add(t);
                return t;
            }

            public override int GetHashCode()
            {
                return base.GetHashCode();
            }

            #region IStateContainer Members

            public object Identifier
            {
                get { return id; }
            }

            public List<Mealy_Transition> Transitions
            {
                get { return tr; }
            }

            public object content
            {
                get { return id; }
                set { this.id = value.ToString(); }
            }

            #endregion
            public override string ToString()
            {
                return id;
            }
        }
        #endregion

        #region Mealy Transition
        /// <summary>
        /// Defenition of Mealy Transition
        /// </summary>
        public class Mealy_Transition //: ITransition<Mealy_State>
        {

            Mealy_State dst;
            PairOfSymbols inputOutput;

            /// <summary>
            /// Constructor
            /// </summary>
            /// <param name="inp">the input symbol</param>
            /// <param name="outp">the output symbol</param>
            public Mealy_Transition(ISymbol inp, ISymbol outp)
            {
                dst = null;
                inputOutput = new PairOfSymbols(inp, outp);
            }

            /// <summary>
            /// Constructor
            /// </summary>
            /// <param name="io">The input/output</param>
            public Mealy_Transition(PairOfSymbols io)
            {
                dst = null;
                inputOutput = io;
            }

            ///// <summary>
            ///// Constructor
            ///// </summary>
            ///// <param name="inp">the input symbol (string)</param>
            ///// <param name="outp">the output symbol (string)</param>
            //public Mealy_Transition(string inp, string outp)
            //{
            //    dst = null;
            //    this.inputOutput = new PairOfStringSymbols(inp, outp);
            //}

            /// <summary>
            /// String representation of a Mealy transition
            /// </summary>
            /// <returns>the string value of this transition</returns>
            public override string ToString()
            {
                try
                {
                    return inputOutput.Input.ToString() + "/" + inputOutput.Output.ToString();
                }
                catch
                {
                    return "";
                }
            }

            /// <summary>
            /// Set destination of a transition
            /// </summary>
            /// <param name="node">the target state</param>
            public void SetDestination(Mealy_State node)
            {
                dst = node;
            }

            /// <summary>
            /// The input symbol of transition
            /// </summary>
            public ISymbol inLabel
            {
                get { return inputOutput.Input; }
            }

            /// <summary>
            /// The output symbol of transition
            /// </summary>
            public ISymbol outLabel
            {
                get { return inputOutput.Output; }
            }

            /// <summary>
            /// The input output symbols as a pair
            /// </summary>
            public PairOfSymbols Label
            {
                get { return inputOutput; }
            }

            #region ITransition Members

            public Mealy_State Destination
            {
                get { return dst; }
            }

            #endregion
        }

        #endregion


        /// <summary>
        /// Constrctor
        /// </summary>
        /// <param name="inputAlphabet">The input alphabet</param>
        /// <param name="outputAlphabet">The output alphabet</param>
        public MealyMachine(Alphabet inputAlphabet = null, Alphabet outputAlphabet = null)
        {
            this.InputAlphabet = inputAlphabet;
            this.OutputAlphabet = outputAlphabet;
        }
		
		public void ComputeOutputAlphabet()
		{
			if(this.OutputAlphabet==null)
				OutputAlphabet = new Alphabet();
			else
				OutputAlphabet.Clear();
			
			foreach(Mealy_State st in states)
			{
				foreach(Mealy_Transition tr in st.Transitions)
				{
					if(!OutputAlphabet.Contains(tr.outLabel))
						OutputAlphabet.AddSymbol(tr.outLabel);
				}
			}
		}
		
		public void ComputeInputAlphabet()
		{
			InputAlphabet.Clear();
			foreach(Mealy_State st in states)
			{
				foreach(Mealy_Transition tr in st.Transitions)
				{
					if(!InputAlphabet.Contains(tr.inLabel))
						InputAlphabet.AddSymbol(tr.inLabel);
				}
			}			
		}
		
		
        /// <summary>
        /// Check weather a state is branching or not
        /// </summary>
        /// <param name="st"></param>
        /// <returns></returns>
        public bool BranchingState(Mealy_State st)
        {
            if (st is Mealy_State)
            {
                foreach (ISymbol s in InputAlphabet.AllSymbols())
                {
                    if ((st as Mealy_State).ListOfAllOutputs(s).Count > 1)
                        return true;
                }
                return false;
            }
            else throw new Exception("Oh! Error...");
        }

        public Alphabet InputAlphabet;

        ///// <summary>
        ///// The input alphabet 
        ///// </summary>
        //public Alphabet InputAlphabet
        //{
        //    get
        //    {
        //        return inputAlphabet;
        //    }
        //}

        /// <summary>
        /// The output alphabet 
        /// </summary>
        public Alphabet OutputAlphabet;

//        /// <summary>
//        /// Read Mealy machine from a DOT file. 
//        /// </summary>
//        /// <param name="inputFile">the full path of input text file</param>
//        /// <returns>the mealy machine</returns>
//        public static MealyMachine ReadFromDOT(string inputFile)
//        {
//            MealyMachine m = new MealyMachine();
//            m.InputAlphabet = new Alphabet();
//            m.OutputAlphabet = new Alphabet();
//
//            DotFormat dotReader = new DotFormat();
//            string ilbl, olbl;
//            foreach (DotFormat.DotTransition tr in dotReader.ReadDotFile(inputFile))
//            {
//                ilbl = tr.Label.Substring(0, tr.Label.IndexOf("/"));
//
//                if (!m.InputAlphabet.Contains(new StringSymbol(ilbl)))
//                    m.InputAlphabet.AddSymbol(new StringSymbol(ilbl));
//
//
//                olbl = tr.Label.Substring(tr.Label.IndexOf("/") + 1, tr.Label.Length - tr.Label.IndexOf("/") - 1);
//
//                if (!m.OutputAlphabet.Contains(new StringSymbol(olbl)))
//                    m.OutputAlphabet.AddSymbol(new StringSymbol(olbl));
//
//                Mealy_State srcNode = null, dstNode = null;
//                foreach (Mealy_State n in m.states)
//                {
//                    if (((string)n.Identifier).Equals(tr.Source))
//                        srcNode = n;
//                    if (((string)n.Identifier).Equals(tr.Destination))
//                        dstNode = n;
//
//                    if (dstNode != null && srcNode != null)
//                        break;
//                }
//                if (srcNode == null)
//                {
//                    srcNode = new Mealy_State(tr.Source);
//                    m.states.Add(srcNode);
//
//                    if (tr.Destination == tr.Source)
//                        dstNode = srcNode;
//                }
//
//                if (dstNode == null)
//                {
//                    dstNode = new Mealy_State(tr.Destination);
//                    m.states.Add(dstNode);
//                }
//
//                Mealy_Transition t = new Mealy_Transition(new StringSymbol(ilbl), new StringSymbol(olbl));
//                t.SetDestination(dstNode);
//                srcNode.Transitions.Add(t);
//            }
//            return m;
//        }

        /// <summary>
        /// Read DFA from a text file. 
        /// <remarks>Each line of file should have the following pattern:
        /// "src" -&gt; "dst" : "label"</remarks>
        /// </summary>
        /// <param name="inputFile">the complete address of input file</param>
        /// <returns>the mealy machine</returns>
        public static MealyMachine readMachine(string inputFile)
        {
            MealyMachine m = new MealyMachine();
            string line;
            m.InputAlphabet = new Alphabet();
            m.OutputAlphabet = new Alphabet();
            if (!System.IO.File.Exists(inputFile))
                throw new Exception("Fatal error: the file '" + inputFile + "' does not exist!");

            // Read the file AND display it line by line.
            System.IO.StreamReader file = new System.IO.StreamReader(inputFile);
            while ((line = file.ReadLine()) != null)
            {
                int i, j;
                i = line.IndexOf("\"");
                j = line.IndexOf("\"", i + 1);
                string src, dst, ilbl, olbl;
                src = line.Substring(i + 1, j - i - 1);

                i = line.IndexOf("->");
                i = line.IndexOf("\"", i + 1);
                j = line.IndexOf("\"", i + 1);
                dst = line.Substring(i + 1, j - i - 1);

                i = line.IndexOf(":");
                i = line.IndexOf("\"", i + 1);
                j = line.IndexOf("\"", i + 1);
                ilbl = line.Substring(i + 1, j - i - 1);

                if (!m.InputAlphabet.Contains(new StringSymbol(ilbl)))
                    m.InputAlphabet.AddSymbol(new StringSymbol(ilbl));


                i = line.IndexOf("-", j);
                i = line.IndexOf("\"", i + 1);
                j = line.IndexOf("\"", i + 1);
                olbl = line.Substring(i + 1, j - i - 1);

                if (!m.OutputAlphabet.Contains(new StringSymbol(olbl)))
                    m.OutputAlphabet.AddSymbol(new StringSymbol(olbl));

                Mealy_State srcNode = null, dstNode = null;
                foreach (Mealy_State n in m.states)
                {
                    if (((string)n.Identifier).Equals(src))
                        srcNode = n;
                    if (((string)n.Identifier).Equals(dst))
                        dstNode = n;

                    if (dstNode != null && srcNode != null)
                        break;
                }
                if (srcNode == null)
                {
                    srcNode = new Mealy_State(src);
                    m.states.Add(srcNode);

                    if (dst == src)
                        dstNode = srcNode;
                }

                if (dstNode == null)
                {
                    dstNode = new Mealy_State(dst);
                    m.states.Add(dstNode);
                }

                Mealy_Transition t = new Mealy_Transition(new StringSymbol(ilbl), new StringSymbol(olbl));
                t.SetDestination(dstNode);
                srcNode.Transitions.Add(t);
            }
            return m;
        }

        //#region Override methods
        //protected override void UpdateTransition(IStateContainer src, ITransition tr, object newTr)
        //{
        //    throw new NotImplementedException();
        //}

        //protected override IStateContainer newStateContainer(object content)
        //{
        //    throw new NotImplementedException();
        //}

        //protected override ITransition newTransition(IStateContainer st, object tr)
        //{
        //    throw new NotImplementedException();
        //}

        //public void AddState(Mealy_State src)
        //{
        //    states.Add(src);
        //}
        //#endregion
    	
    	
		public override MealyMachine.Mealy_State DestinationOf(MealyMachine.Mealy_Transition t)
		{
			return t.Destination;
		}

		public Word Output (Word w)
		{
			Mealy_State tmp = states [0];
			Word o = new Word ();
			for (int i=0; i<w.Length; i++) {
				bool found = false;
				foreach (Mealy_Transition tr in tmp.Transitions) {
					if (tr.inLabel.Equals (w [i])) {
						found = true;
						tmp = tr.Destination;
						o.AddSymbol (tr.outLabel);
						break;
					}
				}
				if (!found)
					throw new Exception ("Opssss!");
			}
			return o;
		}
    }

    /// <summary>
    /// Equivalnce Checker for DFMs and NFMs
    /// </summary>
    public class MM_EquivChecker
    {
        /// <summary>
        /// Find the difference of two deterministic Mealy machines
        /// </summary>
        /// <param name="m1">first machine</param>
        /// <param name="m2">second machine</param>
        /// <returns>a counterexample distinguishing two machines</returns>
        public static Word MM_CheckEquivalence(MealyMachine m1, MealyMachine m2)
        {
            throw new NotImplementedException();
        }

        /// <summary>
        /// Find the difference of two nondeterministic Mealy machines (NFMs)
        /// </summary>
        /// <param name="m1">first machine</param>
        /// <param name="m2">second machine</param>
        /// <returns>a sequence generatable with one machine but not with the other one, null if two are the same</returns>
        public static Sequence NFM_CheckEquivalence(MealyMachine m1, MealyMachine m2)
        {
            throw new NotImplementedException();
        }
    }

}
